rng{i:l}
== {r:rng_sig{i:l}| 
== {ring_p(rng_car(r); rng_plus(r); rng_zero(r); rng_minus(r); rng_times(r); rng_one(r))
== { eqfun_p(rng_car(r); rng_eq(r))}  

latex

Definitions

rng_sig{i:l}, P  Q, ring_p(T; plus; zero; neg; times; one), rng_plus(r), rng_zero(r), rng_minus(r), rng_times(r), rng_one(r), eqfun_p(T; eq), rng_car(r), rng_eq(r)